\begin{tabbing}
$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$).
\\[0ex]atoms{-}distinct(${\it tab}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$x$:Atom1, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it tab}$$\parallel$ }}$.\+
\\[0ex]$n$$\leq$ptr(${\it tab}$)
\\[0ex]$\Rightarrow$ st{-}atom(${\it tab}$;$n$) $=$ $x$
\\[0ex]$\Rightarrow$ \=isl(st{-}lookup(${\it tab}$;$x$))\+
\\[0ex]\& outl(st{-}lookup(${\it tab}$;$x$)) $=$ $\langle$key(${\it tab}$;$n$)$,\,$data(${\it tab}$;$n$)$\rangle$ $\in$ ($\mathbb{N}$+Atom1)$\times$data($T$))
\-\-
\end{tabbing}